\begin{tabbing}
onceR\=\{\$a:ut2, \$done:ut2\}\+
\\[0ex]($i$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=[@$i$ \=precondition for "\$a"(v:Unit):\+\+
\\[0ex]$\lambda$$s$,$v$. $s$."\$done" $=$ false$_{2}$ State("\$done" : $\mathbb{B}$) v
\-\\[0ex]; @$i$ "\$done" initially false$_{2}$:$\mathbb{B}$
\\[0ex]; @$i$ effect locl("\$a")(v:Unit)  "\$done" := $\lambda$$s$,$v$. true$_{2}$ State("\$done" : $\mathbb{B}$) v 
\\[0ex]; @$i$ only events in [locl("\$a")] change "\$done":$\mathbb{B}$])
\-
\end{tabbing}